Unfortunately, Dune >= 3.14 (which includes 3.15.3) is incompatible with the way our continuous integration is setup, as you can see from the failures. (My hypothesis is that dune subst does not support the fact that the home directory contains an opam component.)

Polluting the opam files of coq-core with the upper bound on dune is certainly crude, but it gets the continuous integration running. It would be better to somehow enforce the upper bound in scripts/opam-coq-setup-root, for instance. But nobody investigated how to do that properly.

Doesn't seem to work

The issue is that there are some coq opam packages which do require dune >= 3.14. Also in Coq Platform I had to upgrade to dune 3.15.3 cause of issues.

IMHO it should be discussed with the dune team if the way the CI is setup will permanently be incompatible with dune - in this case the only way is to change the CI setup - or if dune will be made compatible in the near future.

For a few months I can use patched opam files in Coq Platform for the coq packages, but not forever.

cc @rgrinberg

FYI @rgrinberg, the issue at stake would be: ocaml/dune#9895 (comment)

Not sure I really understand the issue, but you might be able to fix if you disable substitution altogether with (subst disabled) in the dune-project file. To help out more, I will need a ticket with a more complete description of the problem.

Closed in favour of #3228 - this follows the approach also used in the Coq released packages.